// Spun AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.IO;
using Formality.FormalSystem.Parser;

namespace Formality.FormalSystem
{
    public class InfixOperator : TermOperator
    {
        public InfixOperator(string Operator, int Precedence, IEnumerable<Proposition> Operands)
            : base(Operator, Operands)
        {
            this.Precedence = Precedence;
        }

        public InfixOperator(string Operator, int Precedence, params Proposition[] Operands)
            : this(Operator, Precedence, (IEnumerable<Proposition>)Operands)
        { }

        public int Precedence { get; private set; }

        public bool IsAxiom { get { return Axioms.Count() > 0; } }
        public bool IsDefinition { get { return Definition != null; } }

        public IEnumerable<Axiom> Axioms
        {
            get
            {
                if (axioms == null)
                    axioms = CalculateAxioms(new Proposition[0]);
                return axioms;
            }
        }
        public Definition Definition { get { return (Definition)this; } }

        #region TermOperator overrides
        protected override TermOperator NewOfThisType(IEnumerable<Proposition> Operands)
        {
            return new InfixOperator(OperatorSymbol, Precedence, Operands);
        }
        #endregion

        #region Sentence overrides
        public override void Serialize(TextWriter Writer, bool Detailed)
        {
            var OpIter = Operands.GetEnumerator();

            var More = OpIter.MoveNext();

            while (More)
            {
                if (Paren(OpIter.Current))
                    Writer.Write("(");

                OpIter.Current.Serialize(Writer, Detailed);

                if (Paren(OpIter.Current))
                    Writer.Write(")");

                if (More = OpIter.MoveNext())
                    Writer.Write(" {0} ", OperatorSymbol);
            }
        }

        public override Inference? Implies(Proposition that, IEnumerable<Sentence> Given)
        {
            var Implication = base.Implies(that, Given);

            if (Implication.HasValue == false && IsAxiom)
            {
                foreach (var Axiom in Axioms)
                {
                    Implication = Axiom.Implies(that, Given);
                    if (Implication.HasValue)
                        break;
                }
            }

            if (Implication.HasValue == false && IsDefinition)
                Implication = Definition.Implies(that, Given);

            return Implication;
        }
        #endregion

        private bool Paren(Proposition Proposition)
        {
            var ThatInfix = Proposition as InfixOperator;

            return (ThatInfix != null && ThatInfix.Precedence <= Precedence);
        }

        public static explicit operator Definition(InfixOperator Op)
        {
            Proposition d1, d2;
            if (AsOperator(Op, SentenceParser.EQ, out d1, out d2))
                return new Definition(d1, d2);
            return null;
        }

        private IEnumerable<Axiom> CalculateAxioms(IEnumerable<Proposition> Antecedents)
        {
            Proposition a, c;
            if (AsOperator(this, SentenceParser.IMPLIES, out a, out c))
            {
                Antecedents = Antecedents.Concat(new[] { a }).ToList();

                yield return new Axiom(Antecedents, c);

                if (c is InfixOperator)
                    foreach (var Axiom in (c as InfixOperator).CalculateAxioms(Antecedents))
                        yield return Axiom;
            }
        }

        private static bool AsOperator(InfixOperator Op, string Operator, out Proposition Arg1, out Proposition Arg2)
        {
            Arg1 = Arg2 = null;

            if (Op.OperatorSymbol == Operator)
            {
                var OpArray = Op.Operands.ToArray();

                if (OpArray.Length == 2)
                {
                    Arg1 = OpArray[0];
                    Arg2 = OpArray[1];
                    return true;
                }
            }

            return false;
        }

        private IEnumerable<Axiom> axioms;
    }
}
